$\forall$${\it es}$:ES, $p$:(E$\rightarrow$(E + Top)).
\\[0ex]causal{-}predecessor(${\it es}$;$p$) $\Rightarrow$ ($\forall$$e$:E. ($\uparrow$can{-}apply($p$;$e$)) $\Rightarrow$ same{-}thread(${\it es}$;$p$;$e$;do{-}apply($p$;$e$)))